Nuprl Definition : atomeqn def 13,42
if a=1 b then x else y is Primitive 
latex

clarification:

atom_eq{$n:n}(a; b; x; y) is Primitive 
latex

Upatoms

origin